e(e1,e2].P(e) == e:es-E(es). ((es-locl(es; e1; e)  es-le(es; e; e2)) c P(e)) 

latex

---

clarification:

existse-between3(es;e1;e2;e.P(e))
== e:es-E(es). ((es-locl(es; e1; e)  es-le(es; e; e2)) c P(e)) 

latex

Definitions	x:A. B(x), es-E(es), A c B, P  Q, es-locl(es; e; e'), es-le(es; e; e')
FDL editor aliases	existse-between3